the_w:World.
FairFifo
 (e, e':E.
 (isrcv(kind(e))
 ( isrcv(kind(e'))
 ( lnk(kind(e)) = lnk(kind(e'))  IdLnk
 ( (e <c e'  sender(e) <c sender(e')  sender(e) = sender(e')  E & index(e)<index(e'))) 

latex

Definitions

Msg, t  T

Lemmas

w-sends-fifo1, Msg sub wf, w-sends-nil, decidable equal Id, w-locl-iff, w-causl wf, filter iseg, decidable le, not functionality wrt iff, map append sq, concat append, concat-cons, append nil sq, top wf, length append, w-onlnk wf, w-m wf, Msg wf, mlnk wf, w-M wf, w-onlnk-m, iseg length, concat wf, concat iseg, map wf, iseg map, w-ml wf, upto wf, upto iseg, decidable lt, filter map upto, assert-eq-lnk, w-kind wf, eqtt to assert, eqff to assert, assert of bnot, bnot wf, not wf, w-isnull wf, bool wf, rcv?-kind, w-loc-lemma, w-loc-rcv, squash wf, true wf, rcv?-link, w-info wf, w-kind-lemma, w-isrcvl wf, w-a wf, assert-w-match, implies functionality wrt iff, iff transitivity, assert of band, assert-eq-id, assert of eq int, iff wf, w-loc wf, band wf, eq id wf, Id wf, eq int wf, lsrc wf, w-action wf, ldst wf, w-rcvs wf, w-snds wf, mu wf, w-match-exists, mu-property, nat wf, le wf, w-match wf, w-time wf, iff functionality wrt iff, or functionality wrt iff, and functionality wrt iff, assert-w-eq-E-iff, w-locl wf, w-eq-E wf, w-index wf, int seg wf, length wf1, w-Msg wf, w-sends wf, w-sender wf, w-E wf, assert wf, isrcv wf, IdLnk wf, lnk wf, w-ekind wf, world wf, fair-fifo wf